$\forall$$T$:Type, ${\it eq}$:EqDecider($T$), $a$:$T$, $L$:$T$ List, $b$:$T$. ($b$ $\in$ insert($a$;$L$)) $\Leftrightarrow$ $b$ $=$ $a$ $\vee$ ($b$ $\in$ $L$)